$\forall$${\it es}$:ES, $i$, $x$:Id, $P$:(\{$e$:E$\mid$ loc($e$) $=$ $i$ \}$\rightarrow$Prop), ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$${\it ds}$($x$)?Top).
\\[0ex]es{-}update{-}iff(${\it es}$;$i$;$x$;${\it ds}$;$e$.$P$($e$);$s$.$f$($s$)) $\in$ Prop